Nuprl Lemma : rel_plus_idempotent
11,40
postcript
pdf
T
:Type,
R
:(
T
T
),
x
,
y
:
T
. (
R
^+(
x
,
y
))
(
R
^+^+(
x
,
y
))
latex
Definitions
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
f
(
a
)
,
R
^+
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
,
R1
=>
R2
,
#$n
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
,
,
{
x
:
A
|
B
(
x
)}
,
a
<
b
,
x
f
y
,
rel_exp(
T
;
R
;
n
)
,
(
i
=
j
)
,
,
A
,
False
,
Void
,
A
B
Lemmas
rel
plus
trans
,
rel
plus
minimal
,
le
wf
,
nat
plus
inc
,
rel
exp
wf
,
rel
plus
monotone
,
rel
plus
wf
origin
T:Type, R:(T
T
), x, y:T. (R^+(x,y)) 
(R^+^+(x,y)) T:Type, R:(TT), x, y:T. (R^+(x,y)) (R^+^+(x,y)) Q Q Qx:A. B(x)B(x)
T
B(x)
x:A. B(x)
j)
A
B